#include "PDTCodeGraph.h"
#include "PDTNode.h"
#include "PDTAssert.h"
#include <saig.h>
#include <abc.h>
#include <abc_global.h>
#include "main.h"
#include "cmd.h"
#include <algorithm>
#include "PDTExpNumBinDerived.h"
#include "PDTNumVar.h"
#include <cmath>
#include <PDTIfElse.h>
#include <PDTWhile.h>
#include <PDTStatement.h>
#include <PDTListOfStatements.h>
#include <PDTExpBoolBinBoolDerived.h>
#include <PDTExpBoolBinNumDerived.h>
#include <PDTCondition.h>
#include <PDTNot.h>

ABC_NAMESPACE_IMPL_START

#include "PDTSCTraversal.h"

#define PDTSCDEBUG 0
#define CONSTDEBUG 0

PDTSCTraversal::PDTSCTraversal(PDTCodeGraph & CG, unsigned int aNodeId, unsigned int aBound, bool aAbc_debug, unsigned int arrBound) : 
    gClone(CG, cg),
    nodeId(aNodeId), 
    size(cg.nodes.size()), 
    bound(aBound), 
    pcTraverse(cg, pc, id2pc),
    arrayBound(arrBound),
    abc_debug(aAbc_debug) {
        PDTAbcZero = NULL;
        PDTAbcOne = NULL;
        size = cg.nodes.size();

        for (unsigned int i = 0; i < size; i++) {
            PDTNode * node = cg.nodes[i];
            if (!node->hasParents()) {
                cout << "***************************************" << endl;
                stringstream ss;
                node->toString(ss);
                cout << ss.str() << endl;
                cout << "***************************************" << endl;
            }
        }

        unsigned int maxArray = (unsigned int) pow (2.0, bound + 0.0); 
        if (arrayBound == 0) {
            cout << "** Warning: Using default value for array bound!" << endl;
            arrayBound = maxArray; 
        } else if (arrayBound > maxArray) {
            cout << "** Warning: Using array bound larger than max " 
                << "possible. Using default value isntead" << endl;
        }

        Abc_Start();
        pAig = Abc_NtkAlloc(ABC_NTK_STRASH,  ABC_FUNC_AIG, 1);
        id2Obj = new PDTAbcObj * [size];
        for (unsigned int i = 0 ; i < size; i++) 
            id2Obj[i] = NULL;
        Abc_Frame_t * pAbc = Abc_FrameGetGlobalFrame();
        Abc_FrameSetCurrentNetwork(pAbc, pAig);

        pc_count = pcTraverse.start();
        if (pc_count == 0) {
            olog() << "Program Counter Traversal Failed!" << endl;
            exit(EXIT_FAILURE);
        }

        unsigned int bits = (unsigned int)ceil(log2(pc_count + 1.0));
        unsigned int len = (unsigned int)pow(2.0, bits + 0.0);
        pc = buildPC(bits);
        pcObjs = new PDTNumAbcObj * [len];
        for (unsigned int i = 0; i < len; i++) {
            pcObjs[i] = NULL;
        }
        PDTBoolAbcObj ovflw;
        pcPlusOne = buildAdder(*pc, *convertConstant(1, bits), ovflw); 

        traverseVariables();
}

PDTSCTraversal::~PDTSCTraversal() {
    Abc_Stop(); // should take care of freeing everything 
    delete [] id2Obj;
}

void
PDTSCTraversal::start() {
    /**
     * Go over all variables and for each variable
     * go over parent assignments and build the pc variable
     */
    for (unsigned int i = 0; i < cg.nodes.size(); i++) {
        PDTNode * node = cg.nodes[i];
        if (!node->hasParents()) {
            if (node->traverseEx(*this) == Stop) {
                olog() << "Received signal Stop from PDTNode having node id = " << 
                    node->getId() << endl;
                
                stringstream ss;
                node->toString(ss);
                cout << "****************************************" << endl;
                cout << ss.str() << endl;;
                cout << "****************************************" << endl;
                break;
            }
        }
    }

    for(unsigned int i = 0; i < cg.variables.size(); i++) {
        PDTVar * var = cg.variables[i];
        PDTNode * node = var->getNode();
        unsigned int pw, mybits;
        mybits = (unsigned int)(ceil(log2(pc_count+1.0)));
        pw = (unsigned int)(pow(2.0, mybits + 0.0));
        if (node->isSequenceVar()) {
            PDTNumArrayObj ** toMux = new PDTNumArrayObj * [pw];
            for (unsigned int p = 0; p < pw; p++)
                toMux[p] = NULL;
            vector < PDTNode * > & parents = node->getParents();

            for (unsigned int j = 0; j < parents.size(); j++) {
                PDTNode * pNode = parents[j];
                if (pNode->isSequenceAccessNum()) {
                    PDTSequenceAccessNum * acc = 
                        (PDTSequenceAccessNum*)pNode;
                    if (!isLHS(*acc))
                        continue;

                    // it is on the left hand side
                    vector <PDTNode*>& accparent = acc->getParents();
                    PDTNode * tNode = accparent[0];
                    if (tNode->isAssign()) {
                        PDTAssign * assign = dynamic_cast<PDTAssign*>(tNode);
                        if (assign == NULL) {
                            olog() << "LHS sequence assign with no parent" << endl;
                            exit(0);
                        }
                        PDTNumArrayObj * muxObj = 
                            dynamic_cast<PDTNumArrayObj *>(id2Obj[pNode->getId()]);
                        unsigned int pcVal = id2pc[assign->getId()]->pre;
                        toMux[pcVal] = muxObj;
                    } else if (tNode->isPiAssign()) {
                        PDTPiAssign * assign = dynamic_cast<PDTPiAssign*>(tNode);
                        if (assign == NULL) {
                            olog() << "LHS sequence assign with no parent" << endl;
                            exit(0);
                        }
                        PDTNumArrayObj * muxObj = 
                            dynamic_cast<PDTNumArrayObj *>(id2Obj[pNode->getId()]);
                        unsigned int pcVal = id2pc[assign->getId()]->pre;
                        toMux[pcVal] = muxObj;
                    }
                }
            }
            PDTNumArrayObj * bos = (PDTNumArrayObj*)id2Obj[node->getId()];
            for (unsigned int k = 0; k < pw; k++) {
                if (toMux[k] == NULL)
                    toMux[k] = bos;
            }
            for (unsigned int v = 0; v < bos->size(); v++) {
                PDTNumAbcObj * vbos = bos->at(v);
                vector <PDTNumAbcObj*> rowVec(pw);
                for (unsigned int idx = 0; idx < pw; idx++) {
                    PDTNumArrayObj * arrObj = toMux[idx];
                    rowVec[idx] = arrObj->at(v);
                }

                vector <PDTNumAbcObj*> retVec(bound);
                for (unsigned int b = 0; b < bound; b++) {
                    retVec[b] = new PDTNumAbcObj(pw);
                }
                transposeVectors(retVec, rowVec, pw);
                PDTNumAbcObj * muxObj = buildMuxVec(retVec, *pc);
                //muxObj should now go as input to variable latch
                PDTNumAbcObj * latches = getFanins(vbos);
                PDTNumAbcObj * bis = getFanins(latches);
                if (!setFanins(bis, muxObj)) {
                    olog() << "Setting array at " << v  
                        << " inputs failed!!" << endl;
                    return;
                }
            }

        } else if (node->isNumVar()) {
            PDTNumAbcObj ** toMux = new PDTNumAbcObj * [pw];
            for (unsigned int p = 0; p < pw; p++)
                toMux[p] = NULL;
            vector < PDTNode * > & parents = node->getParents(); 

            for (unsigned int j = 0; j < parents.size(); j++) {
                PDTNode * pNode = parents[j];
                if (pNode->traverseEx(*this) == Stop) {
                    olog() << "Received signal Stop from PDTNode having node id = " << 
                        pNode->getId() << endl;
                    break;
                }
                if (pNode->isAssign() || pNode->isPiAssign()) {
                    PDTNumAbcObj * muxObj = 
                        dynamic_cast <PDTNumAbcObj*> (id2Obj[pNode->getId()]);
                    unsigned int pcVal = id2pc[pNode->getId()]->pre;
                    toMux[pcVal] = muxObj;
                }
            }
            PDTNumAbcObj * bos = (PDTNumAbcObj*)id2Obj[node->getId()];
            // fill in missing inputs
            for (unsigned int k = 0; k < pw; k++) {
                if (toMux[k] == NULL) {
                    toMux[k] = bos;
                }
            }

            vector < PDTNumAbcObj * > retVec(bound);
            for (unsigned int j = 0; j < bound; j++) {
                retVec[j] = new PDTNumAbcObj(pw);
            }
            transposeVectors(retVec, toMux, pw);
            PDTNumAbcObj * muxObj = buildMuxVec(retVec, *pc);
            //muxObj should now go as input to variable latch
            PDTNumAbcObj * latches = getFanins(bos);
            PDTNumAbcObj * bis = getFanins(latches);
            if (!setFanins(bis, muxObj)) {
                olog() << "Setting variable" << var->getName() 
                    << " inputs failed!!" << endl;
                return;
            }
            //TODO: check if should delete latches and bis

            for (unsigned int j = 0; j < bound; j++) {
                delete retVec[j];
            }
            retVec.clear();
        } else if (node->isBoolVar()) {
            PDTBoolAbcObj ** toMux = new PDTBoolAbcObj * [pw];
            for (unsigned int p = 0; p < pw; p++)
                toMux[p] = NULL;
            vector < PDTNode * > & parents = node->getParents(); 

            for (unsigned int j = 0; j < parents.size(); j++) {
                PDTNode * pNode = parents[j];
                if (pNode->traverseEx(*this) == Stop) {
                    olog() << "Received signal Stop from PDTNode having node id = " << pNode->getId() << endl;
                    break;
                }
                if (pNode->isAssign() || pNode->isPiAssign()) {
                    PDTBoolAbcObj * muxObj = 
                        dynamic_cast <PDTBoolAbcObj*> (id2Obj[pNode->getId()]);
                    unsigned int pcVal = id2pc[pNode->getId()]->pre;
                    toMux[pcVal] = muxObj;
                }
            }
            
            PDTBoolAbcObj * bos = (PDTBoolAbcObj*)id2Obj[node->getId()];
            // fill in missing inputs
            for (unsigned int k = 0; k < pw; k++) {
                if (toMux[k] == NULL) {
                    toMux[k] = bos;
                }
            }
            
            PDTNumAbcObj * temp = new PDTNumAbcObj();
            for (unsigned int i = 0; i < pw; i++) {
                temp->pObjs.push_back(toMux[i]->pBObj);
            }
            
            PDTBoolAbcObj * muxObj = buildMux(*temp, *pc); 
            //muxObj should now go as input to variable latch
            PDTBoolAbcObj * latch = getBoolFanins(bos);
            PDTBoolAbcObj * bis = getBoolFanins(latch);
            if (!setBoolFanins(bis, muxObj)) {
                olog() << "Setting variable" << var->getName() 
                    << " inputs failed!!" << endl;
                return;
            }
            delete temp;
        }
    }

    buildControl();

    for (unsigned int i = 0; i < cg.nodes.size(); i++) {
        unsigned int id = cg.nodes[i]->getId();
        if (id2Obj[id] == NULL) {
            PDTNode * node = cg.nodes[id];
            if (node->isListOfStatements())
                continue;
            cout << "NULL object at id = " << id << endl;
            stringstream ss;
            node->toString(ss);
            cout << ss.str() << endl;
        }
    }
}

void 
PDTSCTraversal::createPOs(PDTNumAbcObj * in, const char * name) {
    vector < Abc_Obj_t * > & inVec = in->pObjs;
    for (unsigned int i = 0; i < in->size(); i++) {
        Abc_Obj_t * pPo = Abc_NtkCreatePo(pAig);
        Abc_ObjAddFanin(pPo, inVec[i]);

        char outName[100];
        //sprintf(outName, "%s-out-%i", name, i);
        sprintf(outName, "%s", name);
        Abc_ObjAssignName(pPo, outName, NULL);
    }
}

void 
PDTSCTraversal::createPIs(PDTNumAbcObj * in, const char * name) {
    vector < Abc_Obj_t * > & inVec = in->pObjs;
    for (unsigned int i = 0; i < in->size(); i++) {
        Abc_Obj_t * pPi = Abc_NtkCreatePi(pAig);
        Abc_ObjAddFanin(inVec[i], pPi);

        char inName[100];
        //sprintf(inName, "%s-in-%i", name, i);
        sprintf(inName, "%s", name);
        Abc_ObjAssignName(pPi, inName, NULL);
    }
}

void
PDTSCTraversal::setUpPcVector(vector < PDTNumAbcObj * > & in) {
    unsigned int bits = (unsigned int)ceil(log2(pc_count + 1.0));
    unsigned int size = (unsigned int)pow(2.0, bits + 0.0);
    for (unsigned int i = 0; i < size; i++) {
        for (unsigned int j = 0; j < pcObjs[i]->size(); j++) {
            in[j]->at(i) = pcObjs[i]->at(j);
        }
    }
}

Traversal::RetType
PDTSCTraversal::post(PDTAssert & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    PDTExpBool * exp = d.getExpression();
    unsigned int expId = exp->getId();
    PDTBoolAbcObj * expObj = (PDTBoolAbcObj*)id2Obj[expId];
    if (expObj == NULL) {
        olog() << "Return error from PDTAssert" << endl;
        return Stop;
    }

    string name = "_assert_";
    ostringstream oss;
    oss << id;
    name += oss.str();
    createPO(expObj, name.c_str());
    id2Obj[id] = expObj;
    return Continue;
}

Traversal::RetType
PDTSCTraversal::post(PDTPreCondition & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    PDTExpBool * exp = d.getExpression();
    unsigned int expId = exp->getId();
    PDTBoolAbcObj * expObj = (PDTBoolAbcObj*)id2Obj[expId];
    if (expObj == NULL) {
        olog() << "Return error from PDTPreCondition" << endl;
        return Stop;
    }

    string name = "_precondition_";
    ostringstream oss;
    oss << id;
    name += oss.str();
    if (abc_debug) {
        createPO(expObj, name.c_str());
    }
    id2Obj[id] = expObj;
    return Continue;
}

Traversal::RetType
PDTSCTraversal::post(PDTPostCondition & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    PDTExpBool * exp = d.getExpression();
    unsigned int expId = exp->getId();
    PDTBoolAbcObj * expObj = (PDTBoolAbcObj*)id2Obj[expId];
    if (expObj == NULL) {
        olog() << "Return error from PDTPostCondition" << endl;
        return Stop;
    }

    string name = "_postcondition_";
    ostringstream oss;
    oss << id;
    name += oss.str();
    if (abc_debug) {
        createPO(expObj, name.c_str());
    }
    id2Obj[id] = expObj;
    return Continue;
}

void
PDTSCTraversal::createPO(PDTBoolAbcObj * in, const char * name) {
    Abc_Obj_t * obj = in->pBObj;
    if (obj == NULL) {
        olog() << "input obj is NULL" << endl;
        return;
    }
    Abc_Obj_t * pPo = Abc_NtkCreatePo(pAig);
    if (pPo == NULL) {
        olog() << "Creating Primary Output failed" << endl;
        return;
    }
    Abc_ObjAddFanin(pPo, obj);

    char outName[100];
    //sprintf(outName, "%s-out", name);
    sprintf(outName, "%s", name);
    Abc_ObjAssignName(pPo, outName, NULL);
}
 
Traversal::RetType 
PDTSCTraversal::post(PDTAdd & d) {
    if (id2Obj[d.getId()] != NULL)
        return Skip;

    PDTAbcObj * abcChild0 = id2Obj[d.getChildEx(0).getId()];
    if (abcChild0->isNull()) {
        olog() << "Traversing parent before child!" << endl;
        return Stop;
    }

    PDTAbcObj * abcChild1 = id2Obj[d.getChildEx(1).getId()];
    if (abcChild1->isNull()) {
        olog() << "Traversing parent before child!" << endl;
        return Stop;
    }

    PDTBoolAbcObj ovflw;
    PDTNumAbcObj * op0 = dynamic_cast<PDTNumAbcObj*>(abcChild0);
    if (op0 == NULL)
        return Stop;
    PDTNumAbcObj * op1 = dynamic_cast<PDTNumAbcObj*>(abcChild1);
    if (op1 == NULL)
        return Stop;
    PDTNumAbcObj * obj = buildAdder(*op0, *op1, ovflw);
    if (obj == NULL)
        return Stop;
    id2Obj[d.getId()] = obj;
    return Continue;  
}
 
Traversal::RetType
PDTSCTraversal::post(PDTNumVar & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;
#if 0
    PDTIntRange * range = d.getRange();
    PDTNumAbcObj * numObj;
    if (range == NULL) 
        numObj = buildVariable(d);
    else  {
        PDTExp * end = range->getEnd();
        if (end->isNumConstInt()) {

        } else  {
            numObj = buildVariable(d);
        }
    }
#endif
    PDTNumAbcObj * numObj = buildVariable(d);
    if (numObj == NULL)
        return Stop;
    id2Obj[id] = numObj;
    string name = d.getName();
    if (abc_debug) {
        createPOs(numObj, name.c_str());
    }
    return Continue;
}

Traversal::RetType
PDTSCTraversal::post(PDTPiAssign & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    // create a PDTAbcObj of Pis and then assign them to this 
    // variable 
    PDTVar * var = d.getTarget();
    PDTNode * node = var->getNode();
    PDTAbcObj * rtrn;
    if (node->isNumVar() || node->isSequenceAccessNum()) {
        PDTNumAbcObj * retObj = new PDTNumAbcObj(bound);

        vector < Abc_Obj_t* > & vObj = retObj->pObjs;
        for (unsigned int i = 0; i < vObj.size(); i++) {
            vObj[i] = Abc_NtkCreatePi(pAig);
        }
        rtrn = retObj;
        id2Obj[id] = retObj;
    } else if (node->isBoolVar() || node->isSequenceAccessBool()) {
        PDTBoolAbcObj * retObj = new PDTBoolAbcObj();

        retObj->pBObj = Abc_NtkCreatePi(pAig);
        rtrn = retObj;
        id2Obj[id] = retObj;
    }

    /* Section 2: Support for sequence access */
    if (!node->isSequenceAccessNum() && !node->isSequenceAccessBool()) 
        return Continue;

    if (node->isSequenceAccessNum()) { 
        PDTSequenceAccessNum * seq = (PDTSequenceAccessNum*)node;
        unsigned int size = seq->getSequenceSize();
        PDTNumArrayObj * container = new PDTNumArrayObj(size);
        vector < PDTNumAbcObj* > & vec = container->pAObjs;

        PDTExpNum * index = seq->getRight();
        unsigned int idx = index->getId();
        PDTNumAbcObj * idxObj = (PDTNumAbcObj*)id2Obj[idx];
        if (idxObj == NULL) {
            olog() << "Sequence Access with undefined index" << endl;
            return Stop;
        }

        PDTSequenceVar * sequence = seq->getLeftVar();
        PDTNumArrayObj * seqObj = (PDTNumArrayObj*)id2Obj[sequence->getId()];
        if (seqObj == NULL) {
            olog() << "Sequence Access with undefined sequence" << endl;
            return Stop;
        }
        PDTNumAbcObj * numObj = (PDTNumAbcObj*)rtrn;

        for (unsigned int i = 0; i < size; i++) {
            PDTNumAbcObj * iObj = convertConstant(i, bound);
            PDTBoolAbcObj * eqObj = eq(iObj, idxObj);
            PDTNumAbcObj * elObj = seqObj->at(i);

            vec[i] = buildOneBitMux(*elObj, *numObj, *eqObj);
        }
        id2Obj[seq->getId()] = container;
        return Continue;
    } else if (node->isSequenceAccessBool()) {
        // TODO: Add support for boolean sequences 
        olog() << "Operation not supported yet" << endl;
#if 0
        PDTSequenceAccessNum * seq = (PDTSequenceAccessNum*)node;
        unsigned int size = seq->getSequenceSize();
        PDTNumArrayObj * container = new PDTNumArrayObj(size);
        vector < PDTNumAbcObj* > & vec = container->pAObjs;

        PDTExpNum * index = seq->getRight();
        unsigned int idx = index->getId();
        PDTNumAbcObj * idxObj = (PDTNumAbcObj*)id2Obj[idx];
        if (idxObj == NULL) {
            olog() << "Sequence Access with undefined index" << endl;
            return Stop;
        }

        PDTSequenceVar * sequence = seq->getLeftVar();
        PDTNumArrayObj * seqObj = (PDTNumArrayObj*)id2Obj[sequence->getId()];
        if (seqObj == NULL) {
            olog() << "Sequence Access with undefined sequence" << endl;
            return Stop;
        }
        PDTNumAbcObj * numObj = (PDTNumAbcObj*)rtrn;

        for (unsigned int i = 0; i < size; i++) {
            PDTNumAbcObj * iObj = convertConstant(i, bound);
            PDTBoolAbcObj * eqObj = eq(iObj, idxObj);
            PDTNumAbcObj * elObj = seqObj->at(i);

            vec[i] = buildOneBitMux(*elObj, *numObj, *eqObj);
        }
        id2Obj[seq->getId()] = container;
        return Continue;
#endif
    }
    return Continue;
}

Traversal::RetType 
PDTSCTraversal::post(PDTAssign & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    PDTNode * expr = d.getExpression();
    PDTAbcObj * obj = id2Obj[expr->getId()];
    if (obj == NULL) {
        olog() << "Traversing parent before child" << endl;
        return Stop;
    }
    id2Obj[id] = obj;

    PDTVar * var = d.getTarget();
    PDTNode * node = var->getNode();
    if (!node->isSequenceAccessNum()) 
        return Continue;

    PDTSequenceAccessNum * seq = (PDTSequenceAccessNum*)node;
    unsigned int size = seq->getSequenceSize();
    PDTNumArrayObj * container = new PDTNumArrayObj(size);
    vector < PDTNumAbcObj* > & vec = container->pAObjs;

    PDTExpNum * index = seq->getRight();
    unsigned int idx = index->getId();
    PDTNumAbcObj * idxObj = (PDTNumAbcObj*)id2Obj[idx];
    if (idxObj == NULL) {
        olog() << "Sequence Access with undefined index" << endl;
        return Stop;
    }

    // Add primay output for checking sequence access violation
    // For now the assumption is that all numbers are positive
    // So will only check if index > seqSize
    // TODO: Make this check an optional addition for the user to 
    // decide whether to do or not.
    unsigned int seqSize = seq->getSequenceSize();
    PDTNumAbcObj * seqSizeObj = convertConstant(seqSize, bound);
    if (seqSizeObj == NULL) {
        olog() << "creating sequence access circuit object failed" << endl;
        return Stop;
    }
    PDTBoolAbcObj * isLarger = gt(idxObj, seqSizeObj); // create the greater than check 
    PDTBoolAbcObj * isEqual = eq(idxObj, seqSizeObj); // create the equal check
    PDTBoolAbcObj * isInBound = new PDTBoolAbcObj();
    Abc_Aig_t * pMan = (Abc_Aig_t*)pAig->pManFunc;
    isInBound->pBObj = Abc_AigOr(pMan, isLarger->pBObj, isEqual->pBObj); // check for gte
    string boundPoName = "_IndexCheck_"; 
    ostringstream oss;
    oss << id;
    boundPoName += oss.str();
    createPO(isInBound, boundPoName.c_str());

    PDTSequenceVar * sequence = seq->getLeftVar();
    PDTNumArrayObj * seqObj = (PDTNumArrayObj*)id2Obj[sequence->getId()];
    if (seqObj == NULL) {
        olog() << "Sequence Access with undefined sequence" << endl;
        return Stop;
    }
    PDTNumAbcObj * numObj = (PDTNumAbcObj*)obj;

    for (unsigned int i = 0; i < size; i++) {
        PDTNumAbcObj * iObj = convertConstant(i, bound);
        PDTBoolAbcObj * eqObj = eq(iObj, idxObj);
        PDTNumAbcObj * elObj = seqObj->at(i);

        vec[i] = buildOneBitMux(*elObj, *numObj, *eqObj);
    }
    id2Obj[seq->getId()] = container;
    return Continue;
}

Traversal::RetType 
PDTSCTraversal::post(PDTNumConstInt & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    PDTNumAbcObj * constObj = convertConstant(d.getValue(), bound);
    if (constObj == NULL) {
        olog() << "Constant creation failed" << endl;
        return Stop;
    }
    id2Obj[id] = constObj;
    return Continue;
}

Traversal::RetType 
PDTSCTraversal::post(PDTBoolConst & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    bool val = d.getValue();
    PDTBoolAbcObj * obj;
    if (val) {
        obj = get1();
    } else {
        obj = get0();
    }
    if (obj == NULL)
        return Stop;
    id2Obj[id] = obj;
    return Continue;
}

void
PDTSCTraversal::traverseVariables() { 
    for (unsigned int i = 0; i < cg.variables.size(); i++) {
        PDTNode *  node = cg.variables[i]->getNode();
        if (node->isVar()) {
            node->traverseEx(*this);
            //post(*numNode);
        }
    }
}

void 
PDTSCTraversal::checkStructure() {
    Abc_AigCleanup((Abc_Aig_t*)pAig->pManFunc);

    if ( !Abc_NtkCheck( pAig ) )
    {
        printf( "The AIG construction has failed.\n" );
        //Abc_NtkDelete( pAig );
    }
}

void 
PDTSCTraversal::Command(const char * cmd) {
    Abc_Frame_t * pAbc = Abc_FrameGetGlobalFrame();
    Cmd_CommandExecute(pAbc, cmd);
}

int 
ConvertBin2Dec(vector <int> & in) {
    if (in.size() == 0)
        return 0;

    unsigned int len = in.size()-1;
    unsigned int result = 0;
    for (int i = len; i >= 0; i--) {
        unsigned int tmp = (unsigned int) pow(2.0, (len-i)*1.0);
        result += in[i] * tmp;
    }
    return result;
}

// Used to automate the sequential prove
void
PDTSCTraversal::PDTProve() {
    string in;
    cout << "##################################################################" << endl
         << "################### This is PDTProve v1.0 ########################" << endl
         << "##################################################################" << endl;
    while(true) {
        cout << "PDTProve >> ";
        getline(cin, in);
        if (in == "start") {
            // First call the balance operation
            cout << "0- Zeroing up all latches: ";
            Command("zero");
            cout << "Zeroing successful" << endl;
            cout << "1- Cleaning up the sequential network: ";
            Command("scleanup");
            cout << "cleanup successful" << endl;
            cout << "2- Balancing the sequential network: ";
            Command("balance");
            cout << "balance successful" << endl;
            cout << "3- Performing dprove on the resulting network" << endl;
            cout << "=============== Result" << endl;
            Command("dprove -vw");
            cout << "=============== End of Result" << endl;
        } else if (in == "show_counter") {
            // write out the counter example
            cout << "Enter the output file name: ";
            getline(cin, in);
            cout << "**** Writing counter example to file " << in << endl;
            string cmd = "write_counter -sn " + in;
            Command(cmd.c_str());
            cout << "*** Writing counter example done." << endl;
        } else if (in == "q" || in == "quit") {
            break;
        }
    }

}

void 
PDTSCTraversal::interActiveCmd() {
    // get input output names
    cout << "========= Getting in_out names =========" << endl;
    Abc_Ntk_t * pNtk = pAig;
    string * pStrIn = new string[Abc_NtkPiNum(pNtk)];
    string * pStrOut = new string[Abc_NtkPoNum(pNtk)];
    string * pStrLatch = new string[Abc_NtkLatchNum(pNtk)];
    PDTAbc_GetIo(pStrIn, pStrOut, pStrLatch, pNtk);
    cout << "== Available Pis:" << endl;
    for (int i = 0; i < Abc_NtkPiNum(pNtk); i++) {
        cout << pStrIn[i] << "\t";
    }
    cout << endl;

    cout << "== Available Pos:" << endl;
    for (int i = 0; i < Abc_NtkPoNum(pNtk); i++) {
        cout << pStrOut[i] << "\t";
    }
    cout << endl;

    cout << "== Available Latches:" << endl;
    for (int i = 0; i < Abc_NtkLatchNum(pNtk); i++) {
        cout << pStrLatch[i] << "\t";
    }
    cout << endl;
    cout << "========================================" << endl;

    // start command line 
    string in;
    while (true) {
        cout << "PDTSC >> ";
        getline(cin, in);
        if (in == "\n")
            continue;
        if (in == "PDTSimulate") {
            int numFrames;
            cout << "Enter the number of frames to run:" << endl;
            getline(cin, in);
            numFrames = atoi(in.c_str());
            cout << "##################################################################" << endl
                 << "################## This is PDTSimulate v1.1 ######################" << endl
                 << "##################################################################" << endl;
            multimap <string, int> mapPi, mapLatch;
            multimap < string, vector<int> > mapPo;
            PDTAbc_NtkXValueSimulate(pAig, numFrames, mapPi, mapPo, mapLatch);
            string in;
            while (true) {
                cout << "PDTSimulate >> ";
                getline(cin, in);
                if (in == "\n")
                    continue;
                else if (in == "q" || in == "quit")
                    break;
                else {
                    pair <multimap<string, int>::iterator, multimap<string, int>::iterator> ret;
                    pair <multimap< string, vector<int> >::iterator, multimap< string, vector<int> >::iterator> poRet;
                    multimap<string, int>::iterator it;
                    cout << "========= " << in << " =========" << endl;
                    ret = mapPi.equal_range(in);
                    for (it = ret.first; it != ret.second; it++) {
                        cout << (*it).second << "\t";
                    }

                    multimap< string, vector<int> >::iterator poIt;
                    poRet = mapPo.equal_range(in);
                    for (poIt = poRet.first; poIt != poRet.second; poIt++) {
                        vector <int> & vec = (*poIt).second;
                        int ret = ConvertBin2Dec(vec);
                        cout << ret << "\t";
                    }

                    ret = mapLatch.equal_range(in);
                    for (it = ret.first; it != ret.second; it++) {
                        cout << (*it).second << "\t";
                    }

                    cout << endl;
                    cout << "================================" << endl;
                }
            }
        }   
        else if (in == "PDTProve")
            PDTProve();
        else if (in == "quit")
            return;
        else 
            Command(in.c_str());
    }
}

int 
ABCMain(const std::string & inputFile, const std::string & funcName, unsigned int scalarBound, unsigned int arrayBound, bool abc_debug) {
    if (abc_debug) {
        cout << "*** Abc Debugging is enabled" << endl;
    }
    PDTCodeGraph * CG = mini_main(inputFile);
    PDTSCTraversal t(*CG, 0, scalarBound, abc_debug, arrayBound);
    t.start();
    t.checkStructure();
    t.interActiveCmd();
    return EXIT_SUCCESS;
}
 
PDTBoolAbcObj * 
PDTSCTraversal::buildMux(PDTNumAbcObj & inps, PDTNumAbcObj & control){
    Abc_Aig_t * aig = (Abc_Aig_t*)(pAig->pManFunc);
    PDTBoolAbcObj * pObj = new PDTBoolAbcObj();
    unsigned int cbound = (int) ceil(log((double)inps.size())/log(2.0));
    if (control.size() < cbound) {
        olog() << "Control not going through all elements" << endl;
        return NULL;
    }
    vector<Abc_Obj_t*> outs;
    for (unsigned int i=0 ;i<inps.size(); i++) {
        Abc_Obj_t* ctrl = NULL;
        int ms = i;
        for (int k=control.size()-1; k>=0; k--) {
            if ((ms&1) == 0) {
                if (ctrl == NULL) {
                    ctrl = Abc_ObjNot(control[k]);
                }   else {
                    ctrl = Abc_AigAnd(aig, ctrl, Abc_ObjNot(control[k]));
                }
            }
            else {
                if (ctrl == NULL) {
                    ctrl = control[k];
                } else {
                    ctrl = Abc_AigAnd(aig, ctrl, control[k]);
                }
            }
            ms = ms >> 1;
        }
        //we created control for mux, now and it, push to vector
        outs.push_back(Abc_AigAnd(aig, ctrl, inps[i]));
    }
    //great we have all the inputs we need to or them
    //smart way to or 2x2
    while (outs.size() > 1) {
        outs.push_back(Abc_AigOr(aig,outs[0], outs[1]));
        outs.erase(outs.begin(), outs.begin()+2);
    }
    pObj->pBObj = outs[0];
    return pObj;
}

PDTNumAbcObj *
PDTSCTraversal::buildMuxVec(vector < PDTNumAbcObj * > & inps, PDTNumAbcObj & control){
    //chooses from inputs given control (big mux)
    PDTNumAbcObj * retObj = new PDTNumAbcObj();
    vector<Abc_Obj_t*> & myret = retObj->pObjs;
    PDTBoolAbcObj * temp;
    for (unsigned int i=0; i<inps.size(); i++) {
        temp = buildMux(*(inps[i]), control);
        myret.push_back(temp->pBObj);
    }
    return retObj; 
}

PDTNumAbcObj * 
PDTSCTraversal::buildVariable(PDTVar & var, unsigned int specialBound) {
    PDTNumAbcObj * obj = new PDTNumAbcObj();
    // create latches
    Abc_Obj_t * pLatch, * pLatchInput, * pLatchOutput;
    vector < Abc_Obj_t * > inputs;
    vector < Abc_Obj_t * > & outputs = obj->pObjs;

    for (unsigned int i = 1; i <= specialBound; i++) {
        pLatch = Abc_NtkCreateLatch(pAig);
        pLatchInput = Abc_NtkCreateBi(pAig);
        pLatchOutput = Abc_NtkCreateBo(pAig);
        Abc_ObjAddFanin(pLatch, pLatchInput);
        Abc_ObjAddFanin(pLatchOutput, pLatch);
        Abc_LatchSetInit0(pLatch); // initialize to 0
        outputs.push_back(pLatchOutput);
        inputs.push_back(pLatchInput);
    }

#if 0
    // create pis and pos and connect them to the latch
    Abc_Obj_t /** pObj;*/ * pObjout;
    for (unsigned int i = 1; i <= bound; i++) {
        // note that index = i - 1 
        // pObj = Abc_NtkCreatePi(pAig);
        // pObj --> inputs[i-1]
        //Abc_ObjAddFanin(inputs[i-1], pObj);

        pObjout = Abc_NtkCreatePo(pAig);
        // outputs[i-1] --> pObjOut
        Abc_ObjAddFanin(pObjout, outputs[i-1]);

        // assign name
        char /*inName[100],*/ outName[100];
        //sprintf(inName, "%s-in-%i", var.getName().c_str(), i-1);
        //Abc_ObjAssignName(pObj, inName, NULL);
        sprintf(outName, "%s-out-%i", var.getName().c_str(), i-1);
        Abc_ObjAssignName(pObjout, outName, NULL);
    }
#endif
    return obj;
}

PDTNumAbcObj * 
PDTSCTraversal::buildVariable(PDTVar & var){
    PDTNumAbcObj * obj = new PDTNumAbcObj();
    // create latches
    Abc_Obj_t * pLatch, * pLatchInput, * pLatchOutput;
    vector < Abc_Obj_t * > inputs;
    vector < Abc_Obj_t * > & outputs = obj->pObjs;

    for (unsigned int i = 1; i <= bound; i++) {
        pLatch = Abc_NtkCreateLatch(pAig);
        pLatchInput = Abc_NtkCreateBi(pAig);
        pLatchOutput = Abc_NtkCreateBo(pAig);
        Abc_ObjAddFanin(pLatch, pLatchInput);
        Abc_ObjAddFanin(pLatchOutput, pLatch);
        Abc_LatchSetInit0(pLatch); // initialize to 0
        outputs.push_back(pLatchOutput);
        inputs.push_back(pLatchInput);
    }
    return obj;
}

PDTNumAbcObj * 
PDTSCTraversal::buildVariable(){
    PDTNumAbcObj * obj = new PDTNumAbcObj();
    // create latches
    Abc_Obj_t * pLatch, * pLatchInput, * pLatchOutput;
    vector < Abc_Obj_t * > inputs;
    vector < Abc_Obj_t * > & outputs = obj->pObjs;

    for (unsigned int i = 1; i <= bound; i++) {
        pLatch = Abc_NtkCreateLatch(pAig);
        pLatchInput = Abc_NtkCreateBi(pAig);
        pLatchOutput = Abc_NtkCreateBo(pAig);
        Abc_ObjAddFanin(pLatch, pLatchInput);
        Abc_ObjAddFanin(pLatchOutput, pLatch);
        Abc_LatchSetInit0(pLatch); // initialize to 0
        outputs.push_back(pLatchOutput);
        inputs.push_back(pLatchInput);
    }

    return obj;
}

PDTNumAbcObj *
PDTSCTraversal::buildPC(unsigned int length) {
    PDTNumAbcObj * obj = new PDTNumAbcObj();
    // create latches
    Abc_Obj_t * pLatch, * pLatchInput, * pLatchOutput;
    vector < Abc_Obj_t * > inputs;
    vector < Abc_Obj_t * > & outputs = obj->pObjs;

    for (unsigned int i = 1; i <= length; i++) {
        pLatch = Abc_NtkCreateLatch(pAig);
        pLatchInput = Abc_NtkCreateBi(pAig);
        pLatchOutput = Abc_NtkCreateBo(pAig);
        Abc_ObjAddFanin(pLatch, pLatchInput);
        Abc_ObjAddFanin(pLatchOutput, pLatch);
        Abc_LatchSetInit0(pLatch); // initialize to 0
        outputs.push_back(pLatchOutput);
        inputs.push_back(pLatchInput);
    }
    
#if 0
    // create pis and pos and connect them to the latch
    Abc_Obj_t * pObj;// * pObjout;
    for (unsigned int i = 1; i <= length; i++) {
        // note that index = i - 1 
        pObj = Abc_NtkCreatePi(pAig);
        // pObj --> inputs[i-1]
        Abc_ObjAddFanin(inputs[i-1], pObj);

        // assign name
        char inName[100];// outName[100];
        sprintf(inName, "pc-in-%i", i-1);
        Abc_ObjAssignName(pObj, inName, NULL);
    }
#endif
    return obj;
}

void
PDTSCTraversal::buildControl() {
    Id2Pc_t::iterator it;
    unsigned int bits = (unsigned int)(ceil(log2(pc_count+1.0)));
    unsigned int size = (unsigned int)pow(2.0, bits + 0.0);
    for (it = id2pc.begin(); it != id2pc.end(); it++) {
        PDTPCHolder * hld = (*it).second;
        unsigned int id = (*it).first;
        if (hld->isPDTIfPCHolder()) {
            /**
             * pre -> (begin_then | begin_else)
             * end_then -> post
             * end_else -> post
             */
            PDTIfPCHolder * ifhld = (PDTIfPCHolder*)id2pc[id];

            pcObjs[ifhld->pre] = (PDTNumAbcObj*)id2Obj[id];

            PDTNumAbcObj * if_post = 
                convertConstant(ifhld->post, bits);
            pcObjs[ifhld->end_then] = if_post;

            pcObjs[ifhld->end_else] = if_post;
        } else if (hld->isPDTWhilePCHolder()) {
            /**
             * pre -> (begin_while | post)
             * end_while -> pre
             */
            PDTWhilePCHolder * whilehld = (PDTWhilePCHolder*)id2pc[id];

            pcObjs[whilehld->pre] = (PDTNumAbcObj*)id2Obj[id];

            PDTNumAbcObj * if_pre = 
                convertConstant(whilehld->pre, bits);
            pcObjs[whilehld->end_while] = if_pre;
        } else {
            /**
             * pre -> post
             */
            PDTNode * node = cg.nodes[id];
            if (node->isListOfStatements())
                continue;
            if (hld->pre == hld->post - 1) {
                pcObjs[hld->pre] = pcPlusOne;
            } else {
                PDTNumAbcObj * post = 
                    convertConstant(hld->post, bits);
                pcObjs[hld->pre] = post;
            }
        }
    }

    // Now build the control mux
    vector < PDTNumAbcObj* > muxIn(bits); 
    for (unsigned int j = 0; j < bits; j++) {
        muxIn[j] = new PDTNumAbcObj(size);
    }

    for (unsigned int i = 0; i < size; i++) {
        if (i < pc_count) {
            if (pcObjs[i] == NULL) {
                pcObjs[i] = pcPlusOne;
            }
        } else {
            PDTNumAbcObj * lastPC = convertConstant(pc_count, bits); 
            if (lastPC == NULL) {
                olog() << "Creating last pc value failed" << endl;
                exit(EXIT_FAILURE);
            }
            pcObjs[i] = lastPC; 
        }
    }
    setUpPcVector(muxIn);

    PDTNumAbcObj * muxObj = buildMuxVec(muxIn, *pc);
    PDTNumAbcObj * latches = getFanins(pc);
    PDTNumAbcObj * bis = getFanins(latches);
    if (!setFanins(bis, muxObj)) {
        olog() << "Setting pc inputs failed!!" << endl;
        return;
    }
    if (abc_debug) {
        createPOs(pc, "PC");
    }
    for (unsigned int j = 0; j < bits; j++) {
        delete muxIn[j];
    }
    muxIn.clear();
}

PDTNumAbcObj * 
PDTSCTraversal::buildAdder(PDTNumAbcObj & inps1, PDTNumAbcObj & inps2, PDTBoolAbcObj & ovflow){
    PDTNumAbcObj * obj = new PDTNumAbcObj();
    vector<Abc_Obj_t *> & myvec = obj->pObjs;
    vector <Abc_Obj_t*> & inps1Vec = inps1.pObjs;
    Abc_Aig_t * pMan = (Abc_Aig_t *)pAig->pManFunc;
    //Adder
    Abc_Obj_t * myxor1, * myxor;
    Abc_Obj_t * myand = get0()->pBObj;
    
    //go through LSB to MSB
    for (int i=inps1Vec.size()-1; i>=0; i--) {
        //output[i] = xor (Cin, A, B)
        myxor1 = Abc_AigXor(pMan, inps1[i], inps2[i]);
        myxor = Abc_AigXor(pMan, myxor1, myand);
        // C = Cin (A xor B)
        myand = Abc_AigAnd(pMan, myand, myxor1);

        //Carry[i] = AB + myand
        myand = Abc_AigOr(pMan, Abc_AigAnd(pMan, inps1[i], inps2[i]), myand);
        //push back sum:
        myvec.push_back(myxor);
    }
    //check carry of last object
    ovflow.pBObj = myand;

    //reverse to make it MSB to LSB
    reverse(myvec.begin(), myvec.end());

#ifndef PDTSCDEBUG
    /**
     * In debug mode, create primary outputs for the adder to
     * check its functionality
     */
    Abc_Obj_t * pObjPo;
    for (unsigned int i = 0; i < myvec.size(); i++) {
        pObjPo = Abc_NtkCreatePo(pAig);
        Abc_ObjAddFanin(pObjPo, myvec[i]);

        char name[100];
        sprintf(name, "%s-%d", "adder", i);
        Abc_ObjAssignName(pObjPo, name, NULL);
    }
#endif

    return obj;
}

PDTBoolAbcObj * 
PDTSCTraversal::get0() {
    if (PDTAbcZero != NULL)
        return PDTAbcZero;

    if (PDTAbcZero != NULL)
        return PDTAbcZero;

    PDTAbcZero = new PDTBoolAbcObj();
    PDTAbcZero->pBObj = Abc_ObjNot(get1()->pBObj);
    return PDTAbcZero;
}

PDTBoolAbcObj * 
PDTSCTraversal::get1(){
    if (PDTAbcOne != NULL)
        return PDTAbcOne;
    
    PDTAbcOne = new PDTBoolAbcObj();
    PDTAbcOne->pBObj = Abc_AigConst1(pAig);
    return PDTAbcOne;
} 

PDTNumAbcObj * 
PDTSCTraversal::getFanins(PDTNumAbcObj * inpt) {
    PDTNumAbcObj * ret = new PDTNumAbcObj();
    vector < Abc_Obj_t * > & retVec = ret->pObjs;

    for (unsigned int i = 0; i < inpt->size(); i++) {
       Vec_Int_t * vec = Abc_ObjFaninVec(inpt->at(i)); 
       for (int j = 0; j < vec->nSize; j++) {
           // vec.nSize should be = 1
           int pos = vec->pArray[j];
           Abc_Obj_t * pObj = Abc_NtkObj(pAig, pos);
           retVec.push_back(pObj);
       }
    }
    return ret;
} 


bool 
PDTSCTraversal::setFanins(PDTNumAbcObj * inpt1, PDTNumAbcObj * fanins) {
    vector <Abc_Obj_t *> & inVec = inpt1->pObjs;
    vector <Abc_Obj_t *> & fanVec = fanins->pObjs; 

    if (inVec.size() != fanVec.size())
        return false;

    for (unsigned int i = 0; i < inVec.size(); i++) {
        Abc_Obj_t * in = inVec[i];
        if (in == NULL)
            return false;
        Abc_Obj_t * fin = fanVec[i];
        if (fin == NULL)
            return false;
        Abc_ObjAddFanin(in, fin);
    }
    return true;
}

PDTNumAbcObj * 
PDTSCTraversal::convertConstant(int myconst, unsigned int aBound) {
    PDTNumAbcObj * pRet = new PDTNumAbcObj();
    vector<Abc_Obj_t*> & zvec = pRet->pObjs;
    int mybound = (int)pow(2, aBound * 1.0);
    if (myconst >= mybound) { 
        olog() << "Constant " << myconst << " not representable in this bound!" << endl;
        olog() << "Exiting! " << endl;
        //TODO: This should be signaled back to the user but doing this now for
        // debuging purposes
        exit(EXIT_FAILURE);
        return pRet;
    }
    mybound = mybound >> 1;
    while (mybound!=0) {
        zvec.push_back(get0()->pBObj);
        mybound = mybound >> 1;
    }
    unsigned int i = zvec.size() -1;
    while (myconst!=0) {
        if ((myconst & 1) == 0) { 
            zvec[i] = get0()->pBObj; 
        } else { 
            zvec[i] = get1()->pBObj; 
        }
        myconst = myconst >> 1;
        i--;
    }
    return pRet;
}

void 
PDTSCTraversal::updatePC() {
    PDTNode * node;
    for (unsigned int i = 0; i < cg.nodes.size(); i++) {
        node = cg.nodes[i];
        updaterVisitNode(node);
    }
}

void
PDTSCTraversal::updaterVisitNode(PDTNode * node) {
    if (id2pc[node->getId()] != NULL)
        return;

    if (node->isAssign()) {
        checkParents(node);
        fixAssign(node);
    } else if (node->isIfElse()) {
        checkParents(node);
        fixIfElse(node);
    } else if (node->isWhile()) {
        checkParents(node);
        fixWhile(node);
    } else { 
        return;
    }
}

void 
PDTSCTraversal::checkParents(PDTNode * node) {
    vector < PDTNode *> & parents = node->getParents();
    if (parents.empty())
        return;

    PDTNode * tmp;
    for (unsigned int i = 0; i < parents.size(); i++) {
        tmp = parents[i];
        if (tmp->isStatement())
            checkParents(tmp);
        updaterVisitNode(tmp);
    }
}

void
PDTSCTraversal::fixAssign(PDTNode * node) {
    assert(node->isAssign());
    unsigned int id = node->getId();
    id2pc[id] = new PCValues_t();
    id2pc[id]->pre = pc_count;
    id2pc[id]->post = ++pc_count;
#if 1
    // print to check for correctness
    cout << "--> " << "pc = " << id2pc[id]->pre << endl;
    stringstream ss;
    node->toString(ss);
    cout << ss.str() << endl;
    cout << "--> " << "pc = " << id2pc[id]->post << endl;
#endif
}

void
PDTSCTraversal::fixIfElse(PDTNode * node) {
    assert(node->isIfElse());
    PDTIfElse * ifptr = (PDTIfElse*)node;
    unsigned int id = node->getId();
    id2pc[id] = new PCValues_t();
    id2pc[id]->pre = pc_count;
    id2pc[id]->post = ++pc_count;
    PDTStatement * stmt = ifptr->getIfResult();
    unsigned int num, eNum;
    // fix then branch
    if (stmt->isListOfStatements()) {
        PDTListOfStatements * stmtList = (PDTListOfStatements*)stmt;
        num = stmtList->numberOfStmts();
    } else {
        num = 1;
    }
    id2pc[id]->post = pc_count + num;

    // fix else branch
    stmt = ifptr->getElseResult();
    if (stmt->isListOfStatements()) {
        PDTListOfStatements * stmtList = (PDTListOfStatements*)stmt;
        eNum = stmtList->numberOfStmts();
    } else if (stmt != &(PDTNilStatement::nil)) {
        eNum = 1;
    } else {
        eNum = 0;
    }
    id2pc[id]->post = pc_count + num + eNum;

#if 1
    // print for correctness
    cout << "--- For if statement: ---" << endl;
    cout << "- PreValue = " << id2pc[id]->pre << endl;
    cout << "- PostValue = " << id2pc[id]->post << endl;
    cout << "- ElseValue = " << id2pc[id]->post << endl;
    cout << "- OutValue = " << id2pc[id]->post << endl;
#endif 
}

void
PDTSCTraversal::fixWhile(PDTNode * node){
    assert(node->isWhile());
    PDTWhile * whileptr = (PDTWhile*)node;
    unsigned int id = whileptr->getId();
    id2pc[id] = new PCValues_t();
    id2pc[id]->pre = pc_count;
    id2pc[id]->post = ++pc_count;
    PDTStatement * stmt = whileptr->getLoopStatement();
    unsigned int num;
    // fix then branch
    if (stmt->isListOfStatements()) {
        PDTListOfStatements * stmtList = (PDTListOfStatements*)stmt;
        num = stmtList->numberOfStmts();
    } else {
        num = 1;
    }
    id2pc[id]->post = pc_count + num;

#if 1
    // print for correctness
    cout << "--- For while statement: ---" << endl;
    cout << "- PreValue = " << id2pc[id]->pre << endl;
    cout << "- PostValue = " << id2pc[id]->post << endl;
    cout << "- OutValue = " << id2pc[id]->post << endl;
#endif 
}

Traversal::RetType 
PDTSCTraversal::post(PDTWhile & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    PDTExpBool * exp = d.getCondition();
    PDTBoolAbcObj * pObj = (PDTBoolAbcObj*)id2Obj[exp->getId()];
    if (pObj == NULL) {
        olog() << "Visiting parent before child" << endl;
        return Stop;
    }

    unsigned int bits = (unsigned int)(ceil(log2(pc_count+1.0)));
    PDTWhilePCHolder * hld = (PDTWhilePCHolder*)id2pc[id];

    PDTNumAbcObj * bg_while = 
        convertConstant(hld->begin_while, bits);
    PDTNumAbcObj * post =
        convertConstant(hld->post, bits);

    PDTNumAbcObj * pRet = 
       buildOneBitMux(*post, *bg_while, *pObj);
    if (pRet == NULL) {
        olog() << "Error Creating PC one bit mux!" << endl;
        return Stop;
    }
    id2Obj[id] = pRet;
    return Continue;

/*
    PCValues_t * whileVal = id2pc[id];
    if (whileVal == NULL) {
        olog() << "PC values for while statement are not yet resolved" << endl;
        return Stop;
    }

    unsigned int whilepre, outpc, whilepc;
    whilepre = whileVal->pre;
    outpc = whileVal->post;
    whilepc = whileVal->post;

    PDTNumAbcObj * pcWhile = convertConstant(whilepc, bits);
    PDTNumAbcObj * pcOut = convertConstant(outpc, bits);
    
    PDTNumAbcObj * pRet = 
        buildOneBitMux(*pcOut, *pcWhile, *((PDTBoolAbcObj*)pObj));
    id2Obj[id] = pRet;
    pcObjs[whilepre] = pRet;

    PDTNumAbcObj * pcPre = convertConstant(whilepre, bits);
    if (pcPre == NULL) {
        olog() << "Creating constant failted" << endl;
        return Stop;
    }
    pcObjs[outpc - 1] = pcPre;
*/
    return Continue;
}

void 
PDTSCTraversal::transposeVectors(vector < PDTNumAbcObj * > & ret, PDTNumAbcObj ** inps, unsigned int size) {
    unsigned int numVec = size;
    // transform them from rows to columns
    for (unsigned int i = 0; i < numVec; i++) {
        for (unsigned int j = 0; j < inps[i]->size(); j++) {
            ret[j]->at(i) = inps[i]->at(j);
        }
    }
}

void
PDTSCTraversal::transposeVectors(vector<PDTNumAbcObj*> & ret, vector<PDTNumAbcObj*> & inps, unsigned int size) {
    unsigned int numVec = size;
    // transform them from rows to columns
    for (unsigned int i = 0; i < numVec; i++) {
        for (unsigned int j = 0; j < inps[i]->size(); j++) {
            ret[j]->at(i) = inps[i]->at(j);
        }
    }
}


PDTBoolAbcObj *
PDTSCTraversal::buildOneBitVar(PDTVar & var) {
    PDTBoolAbcObj * boolptr = new PDTBoolAbcObj();
    Abc_Obj_t * pLatch, * pLatchInput;

    pLatch = Abc_NtkCreateLatch(pAig);
    pLatchInput = Abc_NtkCreateBi(pAig);
    boolptr->pBObj = Abc_NtkCreateBo(pAig);
    Abc_ObjAddFanin(pLatch, pLatchInput);
    Abc_ObjAddFanin(boolptr->pBObj, pLatch);
    Abc_LatchSetInit1(pLatch); // initialize to 0

    return boolptr;
}

PDTBoolAbcObj *
PDTSCTraversal::buildOneBitAndGate(PDTBoolAbcObj & in1, PDTBoolAbcObj & in2) {
    PDTBoolAbcObj * pObj = new PDTBoolAbcObj();

    pObj->pBObj = Abc_AigAnd((Abc_Aig_t*)pAig->pManFunc, in1.pBObj, in2.pBObj);
    if (pObj->pBObj == NULL) {
        olog() << "Creating And gate failed" << endl;
    }
    return pObj;
}

PDTBoolAbcObj *
PDTSCTraversal::buildOneBitOrGate(PDTBoolAbcObj & in1, PDTBoolAbcObj & in2) {
    PDTBoolAbcObj * pObj = new PDTBoolAbcObj();

    pObj->pBObj = Abc_AigOr((Abc_Aig_t*)pAig->pManFunc, in1.pBObj, in2.pBObj);
    if (pObj->pBObj == NULL) {
        olog() << "Creating Or gate failed" << endl;
    }
    return pObj;
}

Traversal::RetType
PDTSCTraversal::post(PDTOr & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
	return Skip;

    PDTAbcObj * abcChild0 = id2Obj[d.getChildEx(0).getId()];
    if (abcChild0->isNull()) {
        olog() << "Traversing parent before child!" << endl;
        return Stop;
    }

    PDTAbcObj * abcChild1 = id2Obj[d.getChildEx(1).getId()];
    if (abcChild1->isNull()) {
        olog() << "Traversing parent before child!" << endl;
        return Stop;
    }

    PDTBoolAbcObj * op0 = dynamic_cast<PDTBoolAbcObj * > (abcChild0);
    PDTBoolAbcObj * op1 = dynamic_cast<PDTBoolAbcObj * > (abcChild1);
    if (op0 == NULL || op1 == NULL)
        return Stop;

    PDTBoolAbcObj * pObj = buildOneBitOrGate(*op0, *op1);
    if (pObj == NULL)
        return Stop;
    id2Obj[id] = pObj;
    return Continue;
}

Traversal::RetType 
PDTSCTraversal::post(PDTAnd & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL) {
        return Skip;
    }
    
    PDTAbcObj * abcChild0 = id2Obj[d.getChildEx(0).getId()];
    if (abcChild0 == NULL) {
        olog() << "Traversing parent before child!" << endl;
        return Stop;
    }

    PDTAbcObj * abcChild1 = id2Obj[d.getChildEx(1).getId()];
    if (abcChild1 == NULL) {
        olog() << "Traversing parent before child!" << endl;
        return Stop;
    }

    PDTBoolAbcObj * op0 = dynamic_cast<PDTBoolAbcObj * > (abcChild0);
    PDTBoolAbcObj * op1 = dynamic_cast<PDTBoolAbcObj * > (abcChild1);
    if (op0 == NULL || op1 == NULL)
        return Stop;

    PDTBoolAbcObj * pObj = buildOneBitAndGate(*op0, *op1);
    if (pObj == NULL)
        return Stop;
    id2Obj[id] = pObj;
    return Continue;
}

Traversal::RetType 
PDTSCTraversal::post(PDTBoolVar & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    PDTBoolAbcObj * boolObj = buildOneBitVar(d);
    if (boolObj == NULL)
        return Stop;
    id2Obj[id] = boolObj;
    //addPi(*boolObj, "tempBool");
    string name = d.getName();
    //addPo(*boolObj, name.c_str());
    return Continue;
}

void
PDTSCTraversal::addPi(PDTBoolAbcObj & boolObj, const char * name) {
   Abc_Obj_t * pPi, * pObj;
   Vec_Int_t * vec;
   int pos;
   pPi = Abc_NtkCreatePi(pAig);

   vec = Abc_ObjFaninVec(boolObj.pBObj); 
   if (vec->nSize > 1) {
       olog() << "Boolean variable has multiple input!" << " Exiting now!" << endl;
       //TODO: think of throwing exceptions here
       exit(EXIT_FAILURE);
   }
   pos = vec->pArray[0];
   pObj = Abc_NtkObj(pAig, pos);

   vec = Abc_ObjFaninVec(pObj);
   if (vec->nSize > 1) {
       olog() << "Boolean variable has multiple input!" << " Exiting now!" << endl;
       //TODO: think of throwing exceptions here
       exit(EXIT_FAILURE);
   }
   pos = vec->pArray[0];
   pObj = Abc_NtkObj(pAig, pos);
       
   char inName[100];
   Abc_ObjAddFanin(pObj, pPi);
   sprintf(inName, "%s-in-0", name);
   Abc_ObjAssignName(pPi, inName, NULL);
}

void
PDTSCTraversal::addPo(PDTBoolAbcObj & boolObj, const char * name) {
   Abc_Obj_t * pPo;
   pPo = Abc_NtkCreatePo(pAig);
   Abc_ObjAddFanin(pPo, boolObj.pBObj);

   char outName[100];
   sprintf(outName, "%s-out-0", name);
   Abc_ObjAssignName(pPo, outName, NULL);
}

Traversal::RetType 
PDTSCTraversal::post(PDTIfElse & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    PDTExpBool * exp = d.getCondition();
    PDTBoolAbcObj * pObj = (PDTBoolAbcObj*)id2Obj[exp->getId()];
    if (pObj == NULL) {
        olog() << "Visiting parent before child" << endl;
        return Stop;
    }

    unsigned int bits = (unsigned int)(ceil(log2(pc_count+1.0)));
    PDTIfPCHolder * ifhld = (PDTIfPCHolder*)id2pc[id];
    PDTNumAbcObj * bg_then = 
        convertConstant(ifhld->begin_then, bits);
    PDTNumAbcObj * bg_else = 
        convertConstant(ifhld->begin_else, bits);

    PDTNumAbcObj * pRet = 
        buildOneBitMux(*bg_else, *bg_then, *pObj);
    if (pRet == NULL) {
        olog() << "Error creating PC one bit Mux!" << endl;
        return Stop;
    }
    id2Obj[id] = pRet;
    return Continue;
}

Traversal::RetType
PDTSCTraversal::post(PDTListOfStatements & d) {
    return Continue;
}

PDTNumAbcObj * 
PDTSCTraversal::buildOneBitMux(PDTNumAbcObj & in0, PDTNumAbcObj & in1, PDTBoolAbcObj
 & cntrl) {
    PDTNumAbcObj * retptr = new PDTNumAbcObj();
    vector < Abc_Obj_t * > & retVec = retptr->pObjs;

    Abc_Obj_t * pC = cntrl.pBObj;
    Abc_Obj_t * tmp;
    for (unsigned int i = 0; i < in0.size(); i++) {
        tmp = Abc_AigMux((Abc_Aig_t *)pAig->pManFunc, pC, in1[i], in0[i]);
        retVec.push_back(tmp); 
    }

    return retptr;
}


Traversal::RetType 
PDTSCTraversal::post(PDTSequenceVar & d) {
    unsigned int id = d.getId();
    unsigned int size = d.getSequence()->getSize();
    if (id2Obj[id] != NULL)
        return Skip;

    if (size == 0) // no size set -> use default
        size = arrayBound;

    PDTNumArrayObj * rObj = new PDTNumArrayObj(size);
    vector < PDTNumAbcObj * > & retVec = rObj->pAObjs;
    
    for (unsigned int i = 0; i < size; i++) {
        PDTNumAbcObj * obj = new PDTNumAbcObj();
        retVec[i] = obj; 
        PDTNumAbcObj * tmpIn = new PDTNumAbcObj();
        // create latches
        vector < Abc_Obj_t * > & inputs = tmpIn->pObjs;
        vector < Abc_Obj_t * > & outputs = obj->pObjs;

        for (unsigned int j = 1; j <= bound; j++) {
            Abc_Obj_t * pLatch, * pLatchInput, * pLatchOutput;
            pLatch = Abc_NtkCreateLatch(pAig);
            pLatchInput = Abc_NtkCreateBi(pAig);
            pLatchOutput = Abc_NtkCreateBo(pAig);
            Abc_ObjAddFanin(pLatch, pLatchInput);
            if (Abc_ObjFanin0(pLatch) == NULL)
                cout << "Found error" << endl;
            
            Abc_ObjAddFanin(pLatchOutput, pLatch);
            if (Abc_ObjFanin0(pLatchOutput) == NULL)
                cout << "Found error on output" << endl;
            Abc_LatchSetInit0(pLatch); // initialize to 0
            outputs.push_back(pLatchOutput);
            inputs.push_back(pLatchInput);
        }
        if (obj == NULL)
            return Stop;
        
        char name[100];
        sprintf(name, "a%d", i);
        //createPIs(tmpIn, name);
        if (abc_debug) {
            createPOs(obj, name);
        }
    }
    id2Obj[id] = rObj;
    return Continue;
}

Traversal::RetType 
PDTSCTraversal::post(PDTSequenceAccessNum & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    // First check whether on right hand side (rhs) or 
    // on left hand side (lhs) and depending on it 
    // act on the sequence and set up the muxes.
    if (!isLHS(d)) { // on the right hand side
        PDTExpNum * cntrl = d.getRight();
        // get the control of the mux
        PDTNumAbcObj * cntrlObj = (PDTNumAbcObj *)id2Obj[cntrl->getId()];
        
        // Add primay output for checking sequence access violation
        // For now the assumption is that all numbers are positive
        // So will only check if index > seqSize
        // TODO: Make this check an optional addition for the user to 
        // decide whether to do or not.
        unsigned int seqSize = d.getSequenceSize();
        PDTNumAbcObj * seqSizeObj = convertConstant(seqSize, bound);
        if (seqSizeObj == NULL) {
            olog() << "creating sequence access circuit object failed" << endl;
            return Stop;
        }
        PDTBoolAbcObj * isLarger = gt(cntrlObj, seqSizeObj); // create the greater than check 
        PDTBoolAbcObj * isEqual = eq(cntrlObj, seqSizeObj); // create the equal check
        PDTBoolAbcObj * isInBound = new PDTBoolAbcObj();
        Abc_Aig_t * pMan = (Abc_Aig_t*)pAig->pManFunc;
        isInBound->pBObj = Abc_AigOr(pMan, isLarger->pBObj, isEqual->pBObj); // check for gte
        string boundPoName = "_IndexCheck_"; 
        ostringstream oss;
        oss << id;
        boundPoName += oss.str();
        createPO(isInBound, boundPoName.c_str());

        PDTSequenceVar * seqVar = d.getLeftVar();
        if (seqVar == NULL) {
            olog() << "Accessing an invalid sequence" << endl;
            return Stop;
        }
        PDTNode * node = seqVar->getNode();
        PDTNumArrayObj * seqObj = (PDTNumArrayObj*)id2Obj[node->getId()];
        vector < PDTNumAbcObj * > & seqVec = seqObj->pAObjs;

        unsigned int size = seqVar->getSequence()->getSize();
        if (size == 0)
            size = arrayBound;

        //TODO: handle case where size < 2^bound
        unsigned int two2bound = (unsigned int)pow(2.0, bound + 0.0);
        if (size < two2bound) {
            cout << "size is less than two to the bound!" << endl;
            cout << "Should handle this!" << endl;
            ; // fill in zeros
        }
        
        vector <PDTNumAbcObj *> retVec(bound);
        for (unsigned int j = 0; j < bound; j++)
            retVec[j] = new PDTNumAbcObj(size);

        transposeVectors(retVec, seqVec, size);
        PDTNumAbcObj * muxObj = buildMuxVec(retVec, *cntrlObj);
        if (muxObj == NULL) {
            olog() << "building index mux for array failed" << endl;
            return Stop;
        }
        id2Obj[id] = muxObj;

        //cleanup
        for (unsigned int k = 0; k < bound; k++)
            delete retVec[k];
        retVec.clear();

        return Continue;
    } else {
        return Skip;
    }
    return Skip;
}

bool
PDTSCTraversal::isLHS(PDTSequenceAccessNum & d) {
    // To check if on the left hand side check for parents 
    // until finding an access node, and then on the access
    // node check whether it is on the lhs (i == 0 or on the
    // rhs (i == 1)
    vector <PDTNode * > & parents = d.getParents();
    for (unsigned int i = 0; i < parents.size(); i++) {
        PDTNode * & node = parents[i];
        if (node->isPiAssign())
            return true;
        if (!node->isAssign())
            continue;
        
        PDTAssign * assign = (PDTAssign*)node;
        PDTVar * trgt = assign->getTarget();
        PDTNode * trgtNode = trgt->getNode();
        if (trgtNode->getId() == d.getId()) {
            return true;
        } else {
            return false;
        }
    }
    return false;
}

Traversal::RetType 
PDTSCTraversal::post(PDTSequenceAccessBool & d) {
    return Skip;
}

PDTBoolAbcObj *
PDTSCTraversal::getBoolFanins(PDTBoolAbcObj * inpt) {
    PDTBoolAbcObj * ret = new PDTBoolAbcObj();
    Abc_Obj_t * & pret = ret->pBObj;

    Vec_Int_t * vec = Abc_ObjFaninVec(inpt->pBObj);
    int pos = vec->pArray[0]; // should not have more elements
    pret = Abc_NtkObj(pAig, pos);

    return ret;
}   

bool
PDTSCTraversal::setBoolFanins(PDTBoolAbcObj * inpt1, PDTBoolAbcObj * fanin) {
    Abc_Obj_t * & inpt = inpt1->pBObj;
    Abc_Obj_t * & fan = fanin->pBObj;

    Abc_ObjAddFanin(inpt, fan);
    return true;
}


PDTBoolAbcObj *
PDTSCTraversal::lt(PDTNumAbcObj * a, PDTNumAbcObj * b) {
    PDTBoolAbcObj * pRet = new PDTBoolAbcObj();

    pRet->pBObj = lt(a,b,0);
    return pRet; 
}

Abc_Obj_t *
PDTSCTraversal::lt(PDTNumAbcObj * a, PDTNumAbcObj * b, unsigned int i) {
    Abc_Aig_t* mman = (Abc_Aig_t*) pAig->pManFunc;
    
    Abc_Obj_t * notAI = Abc_ObjNot(a->at(i));
    Abc_Obj_t * q1 = Abc_AigAnd(mman, notAI, b->at(i));
    if (i == a->size() -1) 
        return q1; 

    Abc_Obj_t *iPlus1 = lt(a, b, i+1);

    Abc_Obj_t *thexor = Abc_AigXor(mman, a->at(i), b->at(i));
    Abc_Obj_t *thexnor = Abc_ObjNot(thexor);
    Abc_Obj_t * big = Abc_AigAnd(mman, thexnor, iPlus1);
    q1 = Abc_AigOr(mman, q1, big);
    return q1; 
}

PDTBoolAbcObj * 
PDTSCTraversal::gt(PDTNumAbcObj * a, PDTNumAbcObj * b) {
    PDTBoolAbcObj * retObj = new PDTBoolAbcObj();
    Abc_Obj_t * _lt = lt(a,b,0);
    Abc_Obj_t * _eq = eq(a,b)->pBObj;

    Abc_Aig_t * mman = (Abc_Aig_t*)pAig->pManFunc;
    Abc_Obj_t * tmp = Abc_AigOr(mman, _lt, _eq);
    retObj->pBObj = Abc_ObjNot(tmp);

    if (retObj->pBObj == NULL) {
        olog() << "Greater then operation failed!" << endl;
        return NULL;
    }
    return retObj;
}

PDTBoolAbcObj * 
PDTSCTraversal::eq(PDTNumAbcObj * a, PDTNumAbcObj * b) {
    Abc_Aig_t* mman = (Abc_Aig_t*) pAig->pManFunc;
    PDTBoolAbcObj * pRet = new PDTBoolAbcObj();
    Abc_Obj_t * & ret = pRet->pBObj;
    vector<Abc_Obj_t*> tocheck;
    for (unsigned int i=0; i<a->size(); i++)
        tocheck.push_back(Abc_AigXor(mman, a->at(i), b->at(i)));

    if (tocheck.size() == 0) return NULL;
    Abc_Obj_t* st = tocheck[0];
    for (unsigned int i=1; i<tocheck.size(); i++) 
        st = Abc_AigOr(mman,tocheck[i], st);
    ret = Abc_ObjNot(st);
    return pRet;
}

Traversal::RetType 
PDTSCTraversal::post(PDTLessThan & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL) {
        return Skip;
    }

    PDTExpNum * left = d.getLeft();
    unsigned int leftId = left->getId();
    PDTExpNum * right = d.getRight();
    unsigned int rightId = right->getId();

    PDTNumAbcObj * leftObj = (PDTNumAbcObj*)id2Obj[leftId];
    PDTNumAbcObj * rightObj = (PDTNumAbcObj*)id2Obj[rightId];
    if (leftObj == NULL ||  rightObj == NULL) {
        olog() << "Traversing parent before traversing child" << endl;
        return Stop;
    }

    PDTBoolAbcObj * retObj;
    retObj = lt(leftObj, rightObj);
    if (retObj == NULL) {
        olog() << "Error creating less than operation" << endl;
        return Stop;
    }

    id2Obj[id] = retObj;
    return Continue;
}

Traversal::RetType
PDTSCTraversal::post(PDTGreaterThan & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL) {
        return Skip;
    }

    PDTExpNum * left = d.getLeft();
    unsigned int leftId = left->getId();
    PDTExpNum * right = d.getRight();
    unsigned int rightId = right->getId();

    PDTNumAbcObj * leftObj = (PDTNumAbcObj*)id2Obj[leftId];
    PDTNumAbcObj * rightObj = (PDTNumAbcObj*)id2Obj[rightId];
    if (leftObj == NULL ||  rightObj == NULL) {
        olog() << "Traversing parent before traversing child" << endl;
        return Stop;
    }

    PDTBoolAbcObj * retObj;
    retObj = gt(leftObj, rightObj);
    if (retObj == NULL) {
        olog() << "Error creating greater than operation" << endl;
        return Stop;
    }

    id2Obj[id] = retObj;
    return Continue;
}

Traversal::RetType
PDTSCTraversal::post(PDTGreaterThanEqual & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL) {
        return Skip;
    }

    PDTExpNum * left = d.getLeft();
    unsigned int leftId = left->getId();
    PDTExpNum * right = d.getRight();
    unsigned int rightId = right->getId();

    PDTNumAbcObj * leftObj = (PDTNumAbcObj*)id2Obj[leftId];
    PDTNumAbcObj * rightObj = (PDTNumAbcObj*)id2Obj[rightId];
    if (leftObj == NULL ||  rightObj == NULL) {
        olog() << "Traversing parent before traversing child" << endl;
        return Stop;
    }

    PDTBoolAbcObj * lessThan= lt(leftObj, rightObj);
    PDTBoolAbcObj * retObj = buildNot(lessThan);

    if (retObj == NULL) {
        olog() << "Error creating greater than operation" << endl;
        return Stop;
    }

    id2Obj[id] = retObj;
    return Continue;
}

Traversal::RetType
PDTSCTraversal::post(PDTLessThanEqual & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
        return Skip;

    PDTExpNum * left = d.getLeft();
    unsigned int leftId = left->getId();
    PDTExpNum * right = d.getRight();
    unsigned int rightId = right->getId();

    PDTNumAbcObj * leftObj = (PDTNumAbcObj*)id2Obj[leftId];
    PDTNumAbcObj * rightObj = (PDTNumAbcObj*)id2Obj[rightId];
    if (leftObj == NULL ||  rightObj == NULL) {
        olog() << "Traversing parent before traversing child" << endl;
        return Stop;
    }

    PDTBoolAbcObj * lessthan = lt(leftObj, rightObj);
    PDTBoolAbcObj * equal = eq(leftObj, rightObj);

    // ret = lessthan or equal
    PDTBoolAbcObj * retObj = buildOneBitOrGate(*lessthan, *equal);
    if (retObj == NULL)
        return Stop;
    
    id2Obj[id] = retObj;
    return Continue; 
}

Traversal::RetType 
PDTSCTraversal::post(PDTEqualNum & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL) {
        return Skip;
    }

    PDTExpNum * left = d.getLeft();
    unsigned int leftId = left->getId();
    PDTExpNum * right = d.getRight();
    unsigned int rightId = right->getId();

    PDTNumAbcObj * leftObj = (PDTNumAbcObj*)id2Obj[leftId];
    PDTNumAbcObj * rightObj = (PDTNumAbcObj*)id2Obj[rightId];
    if (leftObj == NULL ||  rightObj == NULL) {
        olog() << "Traversing parent before traversing child" << endl;
        return Stop;
    }

    PDTBoolAbcObj * retObj;
    retObj = eq(leftObj, rightObj);
    if (retObj == NULL) {
        olog() << "Error creating equal operation" << endl;
        return Stop;
    }

    id2Obj[id] = retObj;
    return Continue;
}

Traversal::RetType
PDTSCTraversal::post(PDTNotEqualNum & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL) {
        return Skip;
    }

    PDTExpNum * left = d.getLeft();
    unsigned int leftId = left->getId();
    PDTExpNum * right = d.getRight();
    unsigned int rightId = right->getId();

    PDTNumAbcObj * leftObj = (PDTNumAbcObj*)id2Obj[leftId];
    PDTNumAbcObj * rightObj = (PDTNumAbcObj*)id2Obj[rightId];
    if (leftObj == NULL ||  rightObj == NULL) {
        olog() << "Traversing parent before traversing child" << endl;
        return Stop;
    }

    PDTBoolAbcObj * equal = eq(leftObj, rightObj);
    PDTBoolAbcObj * retObj = buildNot(equal);
    if (retObj == NULL) {
        olog() << "Error creating equal operation" << endl;
        return Stop;
    }

    id2Obj[id] = retObj;
    return Continue;
}

Traversal::RetType
PDTSCTraversal::post(PDTImplies & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL)
	return Skip;

    PDTExpBool * left = d.getLeft();
    unsigned int leftId = left->getId();
    PDTExpBool * right = d.getRight();
    unsigned int rightId = right->getId();

    PDTBoolAbcObj * leftObj = (PDTBoolAbcObj*)id2Obj[leftId];
    PDTBoolAbcObj * rightObj = (PDTBoolAbcObj*)id2Obj[rightId];
    if (leftObj == NULL || rightObj == NULL) {
	olog() << "sending Stop flag" << endl;
	return Stop;
    }

    // build not(a) or b
    PDTBoolAbcObj * retObj = new PDTBoolAbcObj();
    Abc_Obj_t * tObj;
    Abc_Obj_t * lObj = leftObj->pBObj, * rObj = rightObj->pBObj;
    if (lObj == NULL || rObj == NULL) {
	olog() << "sending Stop flag" << endl;
	return Stop;
    }

    tObj = Abc_ObjNot(lObj); // not a
    retObj->pBObj = Abc_AigOr((Abc_Aig_t*)pAig->pManFunc, tObj, rObj); // not a or b
   
    assert(retObj->pBObj != NULL); 
    id2Obj[id] = retObj;
    return Continue;
}

Traversal::RetType
PDTSCTraversal::post(PDTNot & d) {
    unsigned int id = d.getId();
    if (id2Obj[id] != NULL) 
	return Skip;

    PDTExpBool * dExp = (PDTExpBool*)d.getExpression();
    if (dExp == NULL) {
	olog() << "sending Stop flag" << endl;
	return Stop;
    }

    PDTBoolAbcObj * dObj = (PDTBoolAbcObj*)id2Obj[dExp->getId()];
    if (dObj == NULL) {
	olog() << "sending Stop flag" << endl;
	return Stop;
    }

    PDTBoolAbcObj * pRet = buildNot(dObj);
    assert(pRet != NULL);
    id2Obj[id] = pRet;
    return Continue;
}

PDTBoolAbcObj * 
PDTSCTraversal::buildNot(PDTBoolAbcObj * in) {
    PDTBoolAbcObj * ret = new PDTBoolAbcObj();

    Abc_Obj_t * pIn = in->pBObj;

    ret->pBObj = Abc_ObjNot(pIn);
    if (ret->pBObj == NULL) {
        olog() << "Creating not object failed" << endl;
        return NULL;
    }

    // just in case anything goes wrong
    assert(ret->pBObj != NULL);
    return ret;
}

ABC_NAMESPACE_IMPL_END
